#include "solver.h"

/* restriction of the strong inhibition model */
int sim_model (int N, int L, int pathway[L][N], int S[L][N], int g[N][N], int r[N][N], solver *s, int base)
{
	int i, j, k, t;
	int X1[L - 1], X2[L - 1], Z1[L - 1][N], Z2[L - 1][N]; /* temporary variable */
	int N_var1;

	N_var1 = 2 * (L - 1) + 2 * N * (L - 1);

	for (i = 0; i < L - 1; i++)
	{
		X1[i] = i;
		X2[i] = L - 1 + i;
	}

	for (i = 0; i < L - 1; i++)
	{
		for (j = 0; j < N; j++)
		{
			Z1[i][j] = 2 * (L - 1) + i * N + j;
			Z2[i][j] = 2 * (L - 1) + N * (L - 1) + i * N + j;
		}
	}

	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	/* restriction of our Strong Inhibition Model */
	for (i = 0; i < N; i++)
	{
		for (t = 0; t < L - 1; t++)
		{
			veci_resize (&lits,0);
			var = S[t+1][i];
			veci_push (&lits, toLit (var));
			var = base + N_var1 * i + X1[t];
			veci_push (&lits, toLit (var));
			var = base + N_var1 * i + X2[t];
			veci_push (&lits, toLit (var));
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));

			for (j = 0; j < N; j++)
			{
				veci_resize (&lits,0);
				var = S[t+1][i];
				veci_push (&lits, toLit (var));
				var = base + N_var1 * i + X1[t];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				if (i == j)
				{
					var = r[i][j];
					veci_push (&lits, toLit (var));
				}
				else
				{
					var = g[i][j];
					veci_push (&lits, lit_neg (toLit (var)));
				}
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));
			}

			veci_resize (&lits,0);
			var = S[t+1][i];
			veci_push (&lits, toLit (var));
			var = base + N_var1 * i + X2[t];
			veci_push (&lits, lit_neg (toLit (var)));
			for (j = 0; j < N; j++)
			{
				if (j == i) continue;

				var = base + N_var1 * i + Z1[t][j];
				veci_push (&lits, toLit (var));
			}
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));

			for (j = 0; j < N; j++)
			{
				if (j == i) continue;

				veci_resize (&lits,0);
				var = S[t+1][i];
				veci_push (&lits, toLit (var));
				var = base + N_var1 * i + X2[t];
				veci_push (&lits, lit_neg (toLit (var)));
				var = base + N_var1 * i + Z1[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t+1][i];
				veci_push (&lits, toLit (var));
				var = base + N_var1 * i + X2[t];
				veci_push (&lits, lit_neg (toLit (var)));
				var = base + N_var1 * i + Z1[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = r[i][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));
			}

			veci_resize (&lits,0);
			var = S[t+1][i];
			veci_push (&lits, lit_neg (toLit (var)));
			for (j = 0; j < N; j++)
			{
				var = base + N_var1 * i + Z2[t][j];
				veci_push (&lits, toLit (var));
			}
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));

			for (j = 0; j < N; j++)
			{
				veci_resize (&lits,0);
				var = S[t+1][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = base + N_var1 * i + Z2[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t+1][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = base + N_var1 * i + Z2[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				if (i == j)
				{
					var = r[i][j];
					veci_push (&lits, lit_neg (toLit (var)));
				}
				else
				{
					var = g[i][j];
					veci_push (&lits, toLit (var));
				}
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));
			}

			for (j = 0; j < N; j++)
			{
				if (j == i) continue;

				veci_resize (&lits,0);
				var = S[t+1][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = r[i][j];
				veci_push (&lits, lit_neg (toLit (var)));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));
			}
		}
	}

	veci_delete (&lits);

	return base + N_var1 * N;
}

/* restriction of no quick flips */
void forbidden_quickflips (int N0, int N, int L, int S[L][N], solver *s)
{
	int i, j;

	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	for (i = 0; i < L - 3; i++)
	{
		for (j = N0; j < N; j++)
		{
			veci_resize (&lits,0);
			var = S[i][j];
			veci_push (&lits, toLit (var));
			var = S[i + 1][j];
			veci_push (&lits, lit_neg (toLit (var)));
			var = S[i + 2][j];
			veci_push (&lits, toLit (var));
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));

			veci_resize (&lits,0);
			var = S[i][j];
			veci_push (&lits, lit_neg (toLit (var)));
			var = S[i + 1][j];
			veci_push (&lits, toLit (var));
			var = S[i + 2][j];
			veci_push (&lits, lit_neg (toLit (var)));
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));
		}
	}

	veci_delete (&lits);
}

/* restriction of reliable transisition */
int reliable_trans (int N, int L0, int L, int S[L][N], int g[N][N], int r[N][N], solver *s, int base)
{
	int i, j, k, t;
	int X[L - 2][N], Y[L - 2][N]; /* temporary variable */
	int N_var;

	N_var = 2 * N * (L - 2);

	for (i = 0; i < L - 2; i++)
	{
		for (j = 0; j < N; j++)
		{
			X[i][j] = i * N + j;
			Y[i][j] = N * (L - 2) + i * N + j;
		}
	}

	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	for (i = 0; i < N; i++)
	{
		for (t = L0; t < L - 2; t++)
		{
			veci_resize (&lits,0);
			var = S[t][i];
			veci_push (&lits, toLit (var));
			var = S[t + 1][i];
			veci_push (&lits, lit_neg (toLit (var)));
			for (j = 0; j < N; j++)
			{
				if (i == j)
					continue;

				var = base + N_var * i + X[t][j];
				veci_push (&lits, toLit (var));
			}
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));

			for (j = 0; j < N; j++)
			{
				if (i == j)
					continue;

				veci_resize (&lits,0);
				var = S[t][i];
				veci_push (&lits, toLit (var));
				var = S[t + 1][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = base + N_var * i + X[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t][i];
				veci_push (&lits, toLit (var));
				var = S[t + 1][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = base + N_var * i + X[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 1][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t][i];
				veci_push (&lits, toLit (var));
				var = S[t + 1][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = base + N_var * i + X[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = g[i][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t][i];
				veci_push (&lits, toLit (var));
				var = S[t + 1][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = r[i][j];
				veci_push (&lits, lit_neg (toLit (var)));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t][i];
				veci_push (&lits, toLit (var));
				var = S[t + 1][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 1][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = r[i][j];
				veci_push (&lits, lit_neg (toLit (var)));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));
			}

			/*************************************************/

			veci_resize (&lits,0);
			var = S[t][i];
			veci_push (&lits, lit_neg (toLit (var)));
			var = S[t + 1][i];
			veci_push (&lits, toLit (var));
			var = base + N_var * i + Y[t][i];
			veci_push (&lits, lit_neg (toLit (var)));
			var = r[i][i];
			veci_push (&lits, toLit (var));
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));

			veci_resize (&lits,0);
			var = S[t][i];
			veci_push (&lits, lit_neg (toLit (var)));
			var = S[t + 1][i];
			veci_push (&lits, toLit (var));
			for (j = 0; j < N; j++)
			{
				var = base + N_var * i + Y[t][j];
				veci_push (&lits, toLit (var));
			}
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));

			for (j = 0; j < N; j++)
			{
				if (i == j)
					continue;

				veci_resize (&lits,0);
				var = S[t][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 1][i];
				veci_push (&lits, toLit (var));
				var = base + N_var * i + Y[t][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = g[i][j];
				veci_push (&lits, lit_neg (toLit (var)));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 1][i];
				veci_push (&lits, toLit (var));
				var = base + N_var * i + Y[t][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 1][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = g[i][j];
				veci_push (&lits, lit_neg (toLit (var)));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 1][i];
				veci_push (&lits, toLit (var));
				var = base + N_var * i + Y[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 1][i];
				veci_push (&lits, toLit (var));
				var = base + N_var * i + Y[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 1][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 1][i];
				veci_push (&lits, toLit (var));
				var = base + N_var * i + Y[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = r[i][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));
			}
		}
	}

	return base + N_var * N;
}

/* restriction of convergence */
int convergence (int N, int L0, int L, int S[L][N], int g[N][N], int r[N][N], solver *s, int base)
{
	int i, j, k, t;
	int X[L - 2][N], Y[L - 2][N]; /* temporary variable */
	int N_var;

	N_var = 2 * N * (L - 2);

	for (i = 0; i < L - 2; i++)
	{
		for (j = 0; j < N; j++)
		{
			X[i][j] = i * N + j;
			Y[i][j] = N * (L - 2) + i * N + j;
		}
	}

	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	for (i = 0; i < N; i++)
	{
		for (t = L0; t < L - 2; t++)
		{
			veci_resize (&lits,0);
			var = base + N_var * i + X[t][i];
			veci_push (&lits, lit_neg (toLit (var)));
			var = S[t][i];
			veci_push (&lits, toLit (var));
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));

			veci_resize (&lits,0);
			var = base + N_var * i + X[t][i];
			veci_push (&lits, lit_neg (toLit (var)));
			var = r[i][i];
			veci_push (&lits, lit_neg (toLit (var)));
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));

			veci_resize (&lits,0);
			var = S[t + 1][i];
			veci_push (&lits, lit_neg (toLit (var)));
			var = S[t + 2][i];
			veci_push (&lits, lit_neg (toLit (var)));
			for (j = 0; j < N; j++)
			{
				var = base + N_var * i + X[t][j];
				veci_push (&lits, toLit (var));
			}
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));

			for (j = 0; j < N; j++)
			{
				if (i == j)
					continue;

				veci_resize (&lits,0);
				var = S[t + 1][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 2][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = base + N_var * i + X[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t + 1][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 2][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = base + N_var * i + X[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 1][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t + 1][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 2][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = base + N_var * i + X[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = g[i][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t + 1][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 2][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = r[i][j];
				veci_push (&lits, lit_neg (toLit (var)));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t + 1][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 2][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 1][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = r[i][j];
				veci_push (&lits, lit_neg (toLit (var)));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));
			}

			/*************************************************/

			veci_resize (&lits,0);
			var = S[t + 1][i];
			veci_push (&lits, toLit (var));
			var = S[t + 2][i];
			veci_push (&lits, toLit (var));
			var = base + N_var * i + Y[t][i];
			veci_push (&lits, lit_neg (toLit (var)));
			var = r[i][i];
			veci_push (&lits, toLit (var));
			var = S[t][i];
			veci_push (&lits, lit_neg (toLit (var)));
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));

			veci_resize (&lits,0);
			var = S[t + 1][i];
			veci_push (&lits, toLit (var));
			var = S[t + 2][i];
			veci_push (&lits, toLit (var));
			for (j = 0; j < N; j++)
			{
				var = base + N_var * i + Y[t][j];
				veci_push (&lits, toLit (var));
			}
			begin = veci_begin (&lits);
			solver_addclause (s, begin, begin + veci_size (&lits));

			for (j = 0; j < N; j++)
			{
				if (i == j)
					continue;

				veci_resize (&lits,0);
				var = S[t + 1][i];
				veci_push (&lits, toLit (var));
				var = S[t + 2][i];
				veci_push (&lits, toLit (var));
				var = base + N_var * i + Y[t][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = g[i][j];
				veci_push (&lits, lit_neg (toLit (var)));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t + 1][i];
				veci_push (&lits, toLit (var));
				var = S[t + 2][i];
				veci_push (&lits, toLit (var));
				var = base + N_var * i + Y[t][i];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 1][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = g[i][j];
				veci_push (&lits, lit_neg (toLit (var)));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t + 1][i];
				veci_push (&lits, toLit (var));
				var = S[t + 2][i];
				veci_push (&lits, toLit (var));
				var = base + N_var * i + Y[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t + 1][i];
				veci_push (&lits, toLit (var));
				var = S[t + 2][i];
				veci_push (&lits, toLit (var));
				var = base + N_var * i + Y[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = S[t + 1][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));

				veci_resize (&lits,0);
				var = S[t + 1][i];
				veci_push (&lits, toLit (var));
				var = S[t + 2][i];
				veci_push (&lits, toLit (var));
				var = base + N_var * i + Y[t][j];
				veci_push (&lits, lit_neg (toLit (var)));
				var = r[i][j];
				veci_push (&lits, toLit (var));
				begin = veci_begin (&lits);
				solver_addclause (s, begin, begin + veci_size (&lits));
			}
		}
	}

	return base + N_var * N;
}
